Section: New Results

Formal correctness of embedded programs

Participants : Gilles Dowek [Contact] , Pierre Néron.

Pierre Néron is working on program transformations that remove the operations which create most of the approximations during the computation on floating point numbers, namely square roots and divisions. This kind of formal tool aims at increasing the confidence in embedded programs. The idea of this transformation comes from the elimination of the quantifier on real closed fields, hence the first task is to define a minimal but useful language on which the transformation will apply and then to extend this transformation on formulas to this whole language. Keeping the size of the code produced by this transformation in an acceptable range was a challenging issue in this work. The next objective is to write a formal proof ensuring that the transformation is correct. This work will be done in collaboration with the NASA Langley research center in the Formal Method team: Pierre Néron will visit this center for one month in January 2012.

This work is described in a submitted paper [30] .